Algorithms based on partitioned binary decision diagrams (BDDs) are often used to reduce memory explosion in circuit verification based on BDDs. Because such algorithms tend to suffer from problems associated with scheduling partitions for processing, such algorithms are at times ineffective.